package ewu.expressions

import ewu._
import java.util.ArrayList
import scala.collection.mutable.ArrayBuffer

/**
 * Ein AllQuantor setzt sich aus einer freien Variable, 
 * einem Wertebereich und einer BoolExpression zusammen.
 * 
 * Die freie Variable durchlaeuft den Wertebereich solange, 
 * wie die BoolExpression fuer den Wert gilt und ist genau 
 * dann "true" ist, wenn die BoolExpression "booli" fuer alle 
 * Werte aus der ValueRange "range" gilt.
 * 
 * Ist der Wertebereich leer, so wird eine IllegalArgumentException 
 * geworfen.
 * 
 * Die to*Constructor-Methoden wurden nicht definiert.
 */

case class AllQuantor(variable: String, range: ValueRange, booli: BoolExpression) 
                                          extends Quantor(variable, range, booli) {
  override def toString: String = "(forall " + variable + " in " + 
                                  range.toString + " : " + booli.toString + ")"

  def toAdaConstructor: String = ""

  def toAdaConstructor(t: Int): String = ""

  def toScalaConstructor: String = ""

  def toScalaConstructor(t: Int): String = ""

  def reduce: BoolExpression = booli.reduce

  def isTrue = false

  def evaluate(env: Environment): Option[Boolean] = {
//    if (range.isEmpty) {
//      throw new IllegalArgumentException("Range is empty")
//    }
//    else {
      var end: Boolean = true
      for (i <- range.toScalaRange) {
        if (end) {
          env.addValue(variable, i)
          booli.evaluate(env) match {
            case Some(x) => end &= x

            case _ => null
          }

        }
        else {
          return Some(false)
        }
      }
      return Some(end)

    }
    
  def getVariables(a: ArrayBuffer[Name]) = {
    booli.getVariables(a);
  }
  
  override def replaceVariable(fromVar: Name, toVar: Expression) = {
    booli.replaceVariable(fromVar, toVar);
  }
  
  // Diese Funktion ersetzt diesen Quantor durch eine Funktion fuer die Check-Version.
  override def replaceQuantor(addfuncs: ArrayList[String], arrayvars: ArrayList[String]) 
    : BoolExpression = {
    var tvarsinbooli:ArrayBuffer[Name] = new ArrayBuffer()
    var varsinbooli:ArrayBuffer[Name] = new ArrayBuffer()
    var tpars = ""
    booli.getVariables(tvarsinbooli)
    for(i <- tvarsinbooli) {
      i match {
        case x:ArrayAtIndex =>
          if(!varsinbooli.contains(Name(x.name)) && !x.name.equals(variable)) {
            varsinbooli.append(Name(x.name))
          }
              
        case x:Name => 
          if(!varsinbooli.contains(Name(x.name)) && !x.name.equals(variable)) {
            varsinbooli.append(Name(x.name))
          }           
        case _ =>
      }
    }
    for(i <- varsinbooli) {
      if(arrayvars.contains(i.name))
        tpars += " " + i.name + ": IntArray;"
      else
        tpars += " " + i.name + ": Integer;"
    }
    var ta = new Array[Expression](2 + varsinbooli.length)
    ta(0) = range.fromE
    ta(1) = range.toE
    for(i <- 0 to varsinbooli.length-1) {
      ta(i+2) = varsinbooli(i)
    }
    
    var str = "   FUNCTION forall" + (addfuncs.size+1) + " (rangeS, rangeE: Integer;" + tpars    
    str += ") RETURN Integer IS\n      " + variable + ": Integer = rangeS;\n"
    str += "   BEGIN\n   WHILE " + variable + " <= rangeE LOOP\n"
    str += "         IF not(" + booli.replaceQuantor(addfuncs, arrayvars) + ") THEN\n"
    str += "            RETURN 0;\n         END IF;\n"
    str += "         " + variable + " = " + variable + "+1;\n      END LOOP;\n";
    str += "      RETURN 1;\n"
    str += "   END forall" + (addfuncs.size+1) + ";"
    addfuncs.add(str)

    return new Equal(functionExpression("forall" + addfuncs.size, ta), new Number(1))
  }

//  }
}